Denotational Semantics of Dependent Type Theory
Info. This is a reading course in Denotational Semantics of (Dependent) Type Theory offered as an instance of Specialization in Logic.
Syllabus. (Dependent) Type theory. Categories with Families. Locally cartesian closed categories. Clans and generalized algebraic theories. Natural models. Comprehension categories. Representable map categories.
Audience and Prerequisites. A good knowledge of the language of category theory is a prerequisite for the audience.
-
Category Theory in Context by Emily Riehl.
| Date | Title | |
|---|---|---|
| 1 | (28/02) | Introduction to Homotopy Type Theory, Chap 1. |
| 2 | (07/03) | Syntax and Semantics of Dependent Types |
| 3 | (14/03) | Natural models of homotopy type theory |
| 4 | (21/03) | On the interpretation of Type Theory in locally cartesian closed categories |
| 5 | (28/03) | Duality for Clans: an Extension of Gabriel-Ulmer Duality |
| 6 | (04/04) | A 2-categorical analysis of context comprehension |
| 7 | (11/04) | A General Framework for the Semantics of Type Theory |
Rules. Each student will present their assigned paper. At the end of the course there will be an additional oral exam on an other paper of their choice.
Comments. The course is dense, and has no intention of completely cover the bibliography above. Instead, one of its main intents is to introduce the students to this corpus of knowledge, making sure that they reach a sufficient level of independence and maturity.